1. Field of the Invention
The present invention relates to techniques for verifying designs for digital systems. More specifically, the present invention relates to a method and an apparatus for determining if a trace can be produced by a generator, where the trace is defined as a sequence of assignments to the external interface signals of the generator.
2. Related Art
Verifying a design generally involves deciding whether the design will guarantee that its outputs satisfy some set of properties, under the assumption that its inputs satisfy some other properties. The properties the design is to guarantee are often expressed as checkers, which “observe” the design's input/output behaviors and either “accept” or “reject” the behaviors. Checkers are also referred to as “monitors” or “assertions.”
In contrast, the input behavior that the design can assume is often expressed as a generator, which “produces” legal inputs to the design based on the design's outputs and internal generator states. Hence, the generator provides a general model for the legal environments in which the design is intended to operate.
While checkers and generators are used in different roles in design verification, they share an underlying semantics which defines a set of input/output traces. More specifically, a given set of traces can be expressed either as a generator or as a checker. Deciding which representation to use involves considering two criteria: ease of expression, and tool support for a particular form of representation (checker or generator) in a particular verification role (assumption or guarantee). Neither form of representation is universally easier for expressing traces. For instance, the correctness of a sorting circuit involves two conditions: the values in the output array should vary monotonically with the array indices, and should be a permutation of the sorter's input array. Monotonicity is more easily expressed in the checker representation, while it is easier to use a generator to define the set of input permutations that must contain the sorter's output. There does not seem to be any general rule for predicting which traces will be more easily expressed by which representation. Tool support for the various combinations of role and representation is needed.
Compositional verification is a methodology where verification of a complete system is performed by separately verifying each of the blocks from which the system is constructed. These smaller verification sub-tasks can be much more effective with both simulation and formal tools, mainly because the exposed block interfaces give better controllability and observability. In compositional verification, one block's guarantee is used as a connected block's assumption, and vice versa. Consequently, over the set of block verifications involved in the compositional verification of a system, a single trace set representation will need to be used in both roles, as an assumption and as a guarantee. Thus, the choice of representation for a trace set cannot be governed by tool support for the particular role that trace set will play in any one block's verification, because that trace set will serve the complementary role in some other block's verification.
Tables 1 and 2 summarize the approaches used by these tools to support these representations in the two different roles. In both classes of tools, the generator representation is most natural in the role of block assumption, and the checker representation in the guarantee role. Checkers are also easily incorporated as assumptions in formal verification.
TABLE 1assumptionguaranteecheckerstimulus generationassertiongeneratortestbenchtrace checking
TABLE 2assumptionguaranteecheckerconstraintassertiongeneratortestbenchrefinement checking
Using a checker as an assumption for, which is referred to as “stimulus generation,” has been recently studied by a number of researchers, and a number of solutions have been proposed.
Using a generator as a guarantee is also a non-trivial problem. Note that to simulate against a guarantee represented as a generator, one must test if the trace of a simulation run can be produced by the generator. We refer to the verification problem as “trace checking.” To date, the trace checking problem has not been significantly investigated, and effective solutions have not been developed.
Hence, what is needed is a method and an apparatus for efficiently performing a trace checking operation.